#import "@preview/touying:0.6.1": *
#import themes.aqua: *
#import "@preview/pinit:0.2.2": *

#show: aqua-theme.with(
  aspect-ratio: "16-9",
  config-info(
    title: [概率论],
    subtitle: [Subtitle],
    author: [数学主义],
    date: datetime.today(),
    institution: [Institution],
  ),
)
#set text(font: ("Calibri", "Microsoft YaHei"), weight: "regular", size: 25pt)

#title-slide()

#outline-slide()

// #include "temp.typ"
= 一道作业题
---
#align(center, [#text(size: 90pt)[*怀疑一切！*]])
#align(right, [------马克思的座右铭])

#pause
请先从怀疑你抄的答案开始。

== 题目
<题目>

#text(size: 35pt)[设口袋里有$b$个黑球与$r$个红球. 每次随机取出一个球并放回去,
同时加入$c$个同色球, 其中$c > 0$. 试证明: 对任意正整数$k$而言,
第$k$次取到黑球的概率都是$b \/ \( b + r \)$.]

== 一个错误的证明
<一个错误的证明>
（数学归纳法）设第 $k$ 次取到黑球为事件 $A_k$.

+ 当 $k = 1$ 时， 第一次取到黑球的概率
  $P \( A_1 \) = frac(b, b + r)$，显然成立。

+ 假设 $k = n$ 时结论成立，即 $P \( A_n \) = frac(b, b + r)$.

+ 当 $k = n + 1$ 时， 因为
  $P \( A_n \) = frac(b, b + r)$，$P \( overline(A_n) \) = frac(r, b + r)$，
  $P \( A_(n + 1) divides A_n \) = frac(b + c, b + r + c)$，$P \( A_(n + 1) divides overline(A_n) \) = frac(b, b + r + c)$，
  $ P \( A_(n + 1) \) & = P \( A_n \) P \( A_(n + 1) divides A_n \) + P \( overline(A_n) \) P \( A_(n + 1) divides overline(A_n) \)\
   & = frac(b, b + r) times frac(b + c, b + r + c) + frac(r, b + r) times frac(b, b + r + c)\
   & = frac(b \( b + c \) + r b, \( b + r \) \( b + r + c \))\
   & = frac(b \( b + c + r \), \( b + r \) \( b + r + c \))\
   & = frac(b, b + r) $ 所以 $k = n + 1$ 时结论成立。

因此，第 $k$ 次取到黑球的概率为
$frac(b, b + r)$，$k = 1 \, 2 \, dots.h.c$.

== 第二个错误的证明
<第二个错误的证明>
采用数学归纳法证明。记事件 $A$：取到黑球。

当 $k = 1$ 时，显然：$P_1 \( A \) = frac(b, b + r)$.

假设当 $k = k - 1$ 时，有 $P_(k - 1) \( A \) = frac(b, b + r)$
成立。现证 $P_k \( A \) = frac(b, b + r)$.

若想在第 $k$ 次取到黑球，则有两种情况：

+ 在 $k - 1$ 次时，取到了红球，那么在第 $k$ 次取到黑球的概率为
  $frac(b, b + r + c)$.

+ 在 $k - 1$ 次时，取到了黑球，那么在第 $k$ 次取到黑球的概率为
  $frac(b + c, b + r + c)$.

综上，由全概率公式：
$ P_k \( A \) & = frac(r, b + r) dot.op frac(b, b + r + c) + frac(b, b + r) dot.op frac(b + c, b + r + c)\
 & = frac(b \( b + r + c \), \( b + r \) \( b + r + c \))\
 & = frac(b, b + r) $

即证第 $k$ 次取到黑球的概率为 $frac(b, b + r)$，$k = 1 \, 2 \, dots.h$.

= 概率的连续性
#align(right, [在这里，上下是颠倒的。。。。。。])

== 下连续的定义
<下连续的定义>
设$P$是概率. 如果对任给的一列单调递增的事件${ F_n }$ 

——亦即满足
$F_1 subset F_2 subset dots.h.c subset F_n subset dots.h.c$
的${ F_n }$, 或者说 $F_n arrow.t union.big_(n = 1)^oo F_n$ 

都有
$ lim_(n arrow.r oo) P \( F_n \) = P (union.big_(n = 1)^oo F_n) \, $
我们就说$P$是#strong[下连续]的.

== 上连续的定义
<上连续的定义>
设$P$是概率. 如果当 $ F_n arrow.b inter.big_(n = 1)^oo F_n $ 时必有
$ lim_(n arrow.r oo) P \( F_n \) = P (inter.big_(n = 1)^oo F_n) \, $
我们就说$P$是#strong[上连续]的.

== 概率的连续性
<概率的连续性-1>

#text(size: 50pt)[概率既是下连续的, 又是上连续的.]

== Mathlib4中对应的定理
<mathlib4中对应的定理>
参见
#link("https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/MeasureSpace.html")

```Lean
/-- Continuity from below:
the measure of the union of a directed sequence of (not necessarily measurable) sets
is the supremum of the measures. -/
theorem _root_.Directed.measure_iUnion [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s) :
    μ (⋃ i, s i) = ⨆ i, μ (s i)
```
---
机翻:

```
/-- 下连续：
构成有向序列的（不必可测）的集合的并集的测度等于这些集合的测度的上确界。 -/
定理 _根_.有向.测度_无穷并 [可数 ι] {s : ι → 集合 α} (hd : 有向 (· ⊆ ·) s) :
    μ (⋃ i, s i) = ⨆ i, μ (s i)
```
---
```md
## Implementation notes

Given `μ : Measure α`, `μ s` is the value of the *outer measure* applied to `s`.
This conveniently allows us to apply the measure to sets without proving that they are measurable.
We get countable subadditivity for all sets, but only countable additivity for measurable sets.
```
---
机翻:


*实现说明*

已知`μ : Measure α`，则`μ s`表示对`s`应用*外测度*后得到的值。
这种方式便于我们将测度应用于所有集合，而无需证明这些集合是可测的。
在所有集合上有可数次可加性，但仅在可测集合上才有可数可加性。


== 可列可加=下连续+有限可加
<可列可加下连续有限可加>

#text(size: 40pt)[设$P$是事件域上满足$P \( Omega \) = 1$的非负函数.
那么$P$具有可列可加性的充要条件是它有限可加且下连续.]

= 随机变量的分布函数
== 随机变量的定义
<随机变量的定义>
样本空间$Omega$上的可测函数$X : Omega arrow.r bb(R)$称为#strong[随机变量].

如果$X \( Omega \)$是至多可列集, 就说$X$是#strong[离散]随机变量.

如果$X \( Omega \)$是一个区间, 就说$X$是#strong[连续]随机变量.

== 分布函数的定义
<分布函数的定义>
样本空间$Omega$上的可测函数$X : Omega arrow.r bb(R)$称为#strong[随机变量].

对$x in bb(R)$定义$F \( x \) = P \( X lt.eq x \)$.

我们说函数$F : bb(R) arrow.r bb(R)$是随机变量$X$的#strong[分布函数],
称$X$服从$F \( x \)$, 记为$X tilde.op F \( x \)$.

== Mathlib4中对应的定义
<mathlib4中对应的定义>
参见
#link("https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/CDF.html")

```
/-- Cumulative distribution function of a real measure. The definition currently makes sense only
for probability measures. In that case, it satisfies `cdf μ x = μ.real (Iic x)` (see
`ProbabilityTheory.cdf_eq_real`). -/
noncomputable
def cdf (μ : Measure ℝ) : StieltjesFunction :=
  condCDF ((dirac Unit.unit).prod μ) Unit.unit
```

机翻:

```
/-- 实测度的分布函数。目前该定义仅对概率测度有意义。在此情况下，它满足 `分布函数 μ x = μ.实值 (Iic x)`（参见 `ProbabilityTheory.cdf_eq_real`）。-/
不可计算的
定义 分布函数 (μ : 测度 ℝ) : Stieltjes函数 :=
  条件分布函数 ((单点测度 单元.单元).乘积 μ) 单元.单元
```

== 分布函数的性质
<分布函数的性质>
随机变量$X$的分布函数$F \( x \) = P \( X lt.eq x \)$有三个基本性质:

+ 单调递增.

+ 有界: 恒有$0 lt.eq F \( x \) lt.eq 1$, 并且
  $ lim_(x arrow.r - oo) F \( x \) = 0 \, quad lim_(x arrow.r + oo) F \( x \) = 1 . $

+ 右连续: 对任意$x_0 in bb(R)$都有
  $ lim_(x arrow.r x_0 + 0) F \( x \) = F \( x_0 \) . $
